Current status: For "has effective congruences" there are two unresolved cases left:
category of Banach spaces with linear contractions
category of pseudo-metric spaces with non-expansive maps

(For the second, I think I might be able to adapt the proof of extensive + has effective congruences -> balanced, by considering $(0, 1) \hookrightarrow [0, 1]$ to bound distances within components, then placing copies "far enough" from each other for the construction to still work even if it's not making a coproduct. I'd still have to think about the details and whether they work out. For the first, obviously that trick won't work.)

For "has effective cocongruences" there are still 21 unresolved cases. Among them are Group and Ring which are blockers.

I am not surprised that deciding effective cocongruences for concrete categories is so hard. This amounts to a classification of all cocongruences, and this is hard, as we already saw in Rel for example, but also Set is a good starting point, where it is not trivial. Often we do not even understand all epimorphisms.

I suggest that in this PR we only try to fill the remaining cases where it is required by the unit tests (Grp and Ring).

EDIT. I am pretty confident that for Grp the answer is yes, cocongruences are effective.

Heh, ended up coming back to #114 and also using it to prove elementary topoi have effective cocongruences.

Suggestion. The implication "lsfp → effective congruences" can be refined by "multi-algebraic → effective congruences". Note that the database already includes the implication "lsfp → multi-algebraic". The reference is Thm. 4.0 in Diers's paper (fr) or it's English translation.

I am pretty confident that for Grp the answer is yes, cocongruences are effective.

Do you have any ideas on how we might prove that? So far, I haven't made much progress even on the simplest case I can think of, proving that a cocongruence on $\mathbb{Z}$, $F_2 \twoheadrightarrow E$, necessarily has kernel normally generated by $a^n b^{-n}$ for some $n$.

On Ring I was wondering if the counterexample in CommRing could be adapted there. If I trace through the proofs, I guess the counterexample in CommRing is something like $\mathbb{Z} \times \mathbb{Q} \times \mathbb{Q} \times \mathbb{Z}$ as a cocongruence on $\mathbb{Z} \times \mathbb{Z}$. But then again, if you have two maps $\mathbb{Z} \times \mathbb{Q} \times \mathbb{Q} \times \mathbb{Z} \to R$ then the corresponding idempotents of $R$ don't necessarily have an idempotent as product, so that might not extend to a cocongruence on Ring.

Any other ideas on Ring?

Do you have any ideas on how we might prove that? So far, I haven't made much progress even on the simplest case I can think of, proving that a cocongruence on Z , F 2 ↠ E , necessarily has kernel normally generated by a n b − n for some n .

I don't have a proof for Grp, I just voiced my strong suspicion that it is true. Let me explain this a bit.

Here is a formulation that I find quite instructive: a cocongruence on a group $U$ is a way of putting equivalence relations on the hom-sets $hom(U,G)$ for all groups $G$, such that

• homomorphisms $h : G \to G'$ preserve it
• they are compatible with limits $G = \lim_i G_i$

So we have an equivalence relation $f \sim g$ for homomorphisms $f,g : U \to G$, such that $f \sim g \implies hf \sim hg$ for $h : G \to G'$, and when $G = \lim_i G_i$, then $f \sim g$ iff $p_i f \sim p_i g$ for all $i$.

We also need that the equivalence relation on $hom(U,-)$ is representable, but in many cases this follows because of the limit compatibility. (The only thing left is accessibility, right?)

It is effective when there is a subgroup $V \subseteq U$ such that the equivalence relation is given by $f \sim g \iff f|_V = g|_V$.

(All that holds similarly for general categories, but I find it instructive to write it down in this special case.)

The special case $U = \mathbb{Z}$ means: on the underlying set of any group $G$ we have a natural equivalence relation (we could call it "universal") which is limit-compatible, and we need to find $n \in \mathbb{Z}$ such that it is given by $a \sim b \iff a^n = b^n$. This is an interesting classification result (if true).

And here is why I think it is true: I would literally fall off my chair if somebody writes down an equivalence relation (with the mentioned properties) that does not have this form (for general groups). Yes, this is no proof.

What I find remarkable is that this does not seem to be trivial at all for Ab, but your (almost formal) implication preadditive_kernels_normal_imply_effective_congruences handles this case automatically. Maybe here my POV of ignoring the representable object is not ideal. But still, I think we can use $\mathbb{Q} / \mathbb{Z}$ to find the number $n$, alongside with the lemma that (in the abelian case!) the equivalence relation is actually a subgroup.

From this we get some global $n$ such that $a \sim b \iff a^n = b^n$ when $a$ and $b$ commute. But for non-abelian groups, I have no clue (yet). Since Grp is mono-regular, one can show that the relation descends to subgroups. In particular, it suffices to look at 2-generated groups, at least in theory. Free groups are of no use since here powers cancel.

Random remark: We are proving here that Grp does not satisfy the second half of the definition of being Barr-coexact. But we already know that it is not coregular anyway (the first half of the definition).

Question: I just saw that you have proven that CRing does not have effective cocongruences (using pretopos_balanced), which I find quite surprising. How does the counterexample look like in the description above?

Yes, that's precisely the line of thought I was going along. One thought which occurs is that the equivalence relation of conjugacy is preserved by homomorphisms. However, it's not representable (at least I think it isn't, else you'd essentially get a counterexample to Grp being epi-regular). Another thought: Any proof is going to have to take into account the cotransitivity map in some way. For example, the relation $(a b^{-1})^2 = 1$ is certainly reflexive and symmetric; but it's not transitive, as you can see for example in a dihedral group with $b$ being a reflection and $a,c$ being arbitrary rotations.

As for the example in CRing, I think the counterexample is a corelation on $\mathbb{Z} \times \mathbb{Z}$. I could simplify it a bit by using $\mathbb{Z}[1/2]$ instead of $\mathbb{Q}$. Here $\mathbb{Z} \times \mathbb{Z}$ represents the functor taking a ring to its idempotents; and the equivalence relation represented by $\mathbb{Z} \times \mathbb{Z}[1/2] \times \mathbb{Z}[1/2] \times \mathbb{Z}$ is that two idempotents $e_1, e_2$ are equivalent if and only if 2 is invertible in the rings $e_1 (1-e_2) R$ and $(1-e_1) e_2 R$. I guess the picture under Spec makes it clearer why this is an equivalence relation, involving the cross terms both missing the point $\langle 2\rangle$. Maybe a similar example using $\mathbb{C}[t]$ and $\mathbb{C}[t,1/t]$ would make an example that's easier to think about geometrically, now with two maps to $\mathbb{A}^1+\mathbb{A}^1$ being equivalent if the projections to $\mathbb{A}^1$ are equal and if the cross terms both miss 0. Except algebraically that complicates the picture because now you also have to keep track of elements of the ring along with idempotents, and maybe now you want $a=b$, and for $e_1 (1-e_2) a$ and $(1-e_1) e_2 a$ to be units in their respective rings.

Anyway, as far as I can tell, all that breaks down completely in noncommutative rings since you no longer have $eR$ forming a sub-rng.

Ok. I haven't thought about this long, but why cannot we take $eRe$?

Also, images of two commuting idempotents are still commuting. So their product is still idempotent.

For groups, the conjugation relation is not limit-preserving. I think we can say straight away that the equivalence relation must be some algebraic equation.

Hmm... OK, I guess maybe an idempotent would split a ring into $\begin{bmatrix} eRe & (1-e)Re \ eR(1-e) & (1-e)R(1-e) \end{bmatrix}$ or something along those lines.

For the comments on groups: yes, certainly in the general case if you take a presentation $(A, R)$ of $X$, then from generators of the kernel of $FA+FA \to E$ you get some algebraic equations in terms of some number of paired variables, which form an equivalence on tuples satisfying the relations $R$. EDIT: For a slightly different point of view but equivalently, the equations define a partial equivalence relation whose natural domain is the tuples satisfying the relations from $R$. (Of course that description only works for algebraic categories which are epi-regular.) The thing is that those equations could nomimally involve cross terms and the proof would have to find some way to detangle the cross terms, either implicitly or explicitly. The example I have in mind is that $E := \langle a, b \mid b^{-1} a = b a^{-1} \rangle$ as a corelation on $\mathbb{Z}$ is a disguised version of the relation $a^2 = b^2$. (I guess maybe that's another reason why the proof is so easy in R-Mod: you can just move cross terms to the other side. :) )

For another example I have in mind, in the full subcategory of integral (or cancellative) commutative monoids, the equivalence $(a, b) \sim (c, d)$ if and only if $a+d = b+c$ is representable, but not effective. Of course, there's no reason to believe that category is particularly well-behaved...

Still no progress on the case of Ring. Time to see if anybody on MO has any ideas?

I also had the idea of trying to create a counterexample in CMon based on the counterexample in CRing with $\mathbb{Z}[t] \hookrightarrow \mathbb{Z}[t,1/t]$. That doesn't quite seem to be working out for the conditions involving $1-e$. On the other hand, maybe I should have expected such attempts wouldn't be that easy, based on the fact that CMon is not even codistributive, much less coextensive.

For some minor comments on the CRing case regarding the counterexample there:

Geometrically under the image of Spec, the equivalence relation is that (2) maps to the same component of Spec ( Z ) ⊔ Spec ( Z ) under both maps.

The purely algebraic proof that it works as an equivalence relation: e 1 ( 1 − e 3 ) = e 1 e 2 ( 1 − e 3 ) + e 1 ( 1 − e 2 ) ( 1 − e 3 ) , so we can take e 1 times the inverse of 2 in e 2 ( 1 − e 3 ) R plus ( 1 − e 3 ) times the inverse of 2 in e 1 ( 1 − e 2 ) R as an inverse of 2 in e 1 ( 1 − e 3 ) R ; and similarly for ( 1 − e 1 ) e 3 R .

I don't have enough context to understand what you are writing here (which is a general problem in our communication, I must say). "both maps" -> which maps? Can you please start the example from scratch?

Still no progress on the case of Ring. Time to see if anybody on MO has any ideas?

Yes, you can ask. 👍🏼 To be honest, I have no idea for this category.

https://mathoverflow.net/questions/510744/does-the-category-of-rings-have-effective-cocongruences

While we are waiting for MO, maybe there is a chance to handle some of the other categories?

Unknown categories for "effective congruences":

• Ban*
• PMet*

Unknown categories for "effective cocongruences":

• Alg
• Ban
• CMon
• FinGrp*
• Haus*
• LRS
• Met_c
• Met
• Met_oo
• Mon
• Pos*
• Ring
• Rng
• Sch
• Cat

*These categories look doable.

I'll take a closer look at the comments this evening. For now, I think among the (easy to trivial) lemmas I'll use to plug the gaps in proofs for subcategories will be: If $f, g : E \rightrightarrows X$ is a congruence which has a quotient $p : X \to X/E$ and which is effective, then in fact we get a cartesian square with $f, g, p, p$. And: If $U : \mathcal{C} \to \mathcal{D}$ is fully faithful, and $U$ applied to a square (not necessarily even a commutative square in the assumptions) gives a cartesian square, then the original square was cartesian as well.

So, for example, the proof that FinGrp has effective congruences would be: take the coequalizer in the category of groups, which is finite; then we get a cartesian square in Grp involving the quotient; so we also get the required cartesian square in FinGrp.